M:k may not read x
== x  dom((M.2.2.2.2.2.2.2.2.2.2).1)  (deq-member(KindDeq;k;(M.2.2.2.2.2.2.2.2.2.2).1(x))) 

latex

---

clarification:

M:k may not read x
== fpf-dom(IdDeq; x; ((M.2.2.2.2.2.2.2.2.2.2).1))
==  (deq-member(KindDeq;k;(M.2.2.2.2.2.2.2.2.2.2).1IdDeq(x))) 

latex

Definitions	p  q, x  dom(f), b, deq-member(eq;x;L), KindDeq, f(x), t.1, t.2, IdDeq
FDL editor aliases	ma-no-read